\begin{tabbing}
f{-}msg\=\{\$wanted:ut2, \$free:ut2, \$z:ut2\}\+
\\[0ex](${\it es}$; $L$; $e$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(loc($e$) $\in$ $L$)\+
\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]c$\wedge$ \=(((es{-}tag(${\it es}$; $e$) = mkid\{\$wanted:ut2\}) $\vee$ (es{-}tag(${\it es}$; $e$) = mkid\{\$free:ut2\}))\+
\\[0ex]$\wedge$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$) $\wedge$ ($\neg$($i$ = loc($e$))) $\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, loc($e$), mkid\{\$z:ut2\}$>$)))))
\-\-\-\-
\end{tabbing}